/* 
 * Copyright 2014 Josef Hertl.
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package caetus.modelChecking.role;

import caetus.modelChecking.transition.TransitionAction;
import caetus.modelChecking.transition.TransitionActionEnum;
import caetus.modelChecking.transition.TransitionMaker;
import caetus.modelChecking.variable.ModelBaseVariable;
import caetus.modelChecking.variable.ModelVariable;
import caetus.modelChecking.variable.ModelVariableType;
import caetus.pkcs11.tokenCapabilities.TokenCapabilities;
import caetus.pkcs11.tokenCapabilities.TokenCapability;

/**
 * Represents a person - usually an intruder.
 *
 * @author Josef Hertl
 */
public class ModelPerson extends ModelActor {

    public ModelPerson(ModelVariable playedByAgent, String name, TokenCapabilities capabilities) {
        super(playedByAgent, name, capabilities);
    }

    @Override
    protected String makeTransitions() {
        String result = "\ntransition\n\n";
        int ordinal = 1;
        //Simply generates a secret key EK that is saved as local variable and can be worked with later
        if (capabilities.capabilityWorking(TokenCapability.SYMMETRIC_ENCRYPTION_DECRYPTION)) {
//            result += TransitionMaker.makeStatelessTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("ESKSK"), true), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("ESKSK"), true)});
//            ordinal++;
        }

        result += TransitionMaker.makeStatelessTransition(ordinal, new TransitionAction(TransitionActionEnum.RECEIVE_VARIABLE, findVariable("M"), true), new TransitionAction[]{new TransitionAction(TransitionActionEnum.SEND_PLAIN, findVariable("M"))});
        ordinal++;

        return result;
    }

    @Override
    public void generateLocalVariables() {
        addLocalVariable(new ModelBaseVariable("M", ModelVariableType.MESSAGE));
    }
}
